1. Field of the Invention
The present invention relates to an automatic design apparatus, an automatic design method, and an automatic design program of a digital circuit that automatically design a control apparatus to meet a predetermined control specification.
2. Description of the Related Art
As the density of an integrated circuit increases, design data of integrated circuits is increasingly reused when designing an integrated circuit. In an integrated circuit design field, the design property that can be reused is referred to as intellectual property (IP).
In a system level design of an integrated circuit that has been recently used, a method is proposed in which a design of an arithmetic function is separated from, for example, a design of a communication interface in order to increase the reusability of IP and decrease the burden on verification.
The design of an interface circuit is a work that easily causes a designer to make an error. This design requires an accurate description of operation timings with consideration of various inputs from other modules operating in parallel. Even when the design is sufficiently carefully created, an erroneous operation under a specific condition cannot be completely avoided.
For this reason, in general, the design result is verified meticulously. Examples of the verification include simulation-based verification and formal verification.
The simulation-based verification requires an input for the examination (i.e., test vector). To create the test vector requires another effort in addition to the design work. Additionally, the simulation-based verification requires significant effort to check the result of simulation. Furthermore, to exhaustively verify even a rare situation, an enormous amount of time is required.
Property checking is one type of the formal verification. The property checking is a method in which, by defining a specification (property) that describes the desired circuit operations, it is automatically examined whether the design result satisfies the property. The property checking eliminates the need for test vectors. In addition, the property checking can exhaustively verify even a rare situation. Thus, in recent years, the property checking has drawn attention.
In general, the property is written in a language based on a temporal logic (a logical system that handles logical statements of Boolean algebra enhanced with temporal operators). Examples of such a language include the PSL and the SystemVerilog Assertion.
In verification of an interface circuit, defects that exceptionally cause an incorrect operation are found, and therefore, the property checking is suitable. Additionally, since, in many cases, an interface circuit employs the bus standard and the frequently used interface format, a predefined property can be applied. As a result, the number of required steps for the verification can be reduced.
However, the simulation-based verification and the property checking provide only a method for verifying the design result. If a design error is found, the design is corrected and the verification is carried out again. This procedure requires a large amount of manpower. Accordingly, there is need for a method that automatically acquires a model of a control apparatus (interface circuit), like a design method of a control system described below.
In particular, in many cases of designing an interface circuit, the control specification (property) can be prepared in advance. Accordingly, an automatic design of a control system can significantly facilitate the verification.
In general, a digital apparatus can be modeled as a discrete event system. Among discrete event systems, the simplest and widely used system is a finite state machine (FSM). Many types of FSMs are available. For example, an automaton, a sequential machine, and a Kripke structure belong to an FSM.
The automaton is used as a language model in a language theory. The Kripke structure is used as a temporal logic model in a logical theory. The sequential machine is used as a digital circuit model.
One of the basic technologies for generating a model of a control apparatus is described by Sunil P. Khatri, Amit Narayan, Sriram C. Krishnan, Kenneth L. McMillan, Robert. K. Brayton, and A. Sangiovanni-Vincentelli, “Engineering Change in a Non-Deterministic FSM Setting”, Proceedings of the 33rd annual conference on Design automation, pp. 451-456, ISBN: 0-89791-779-0, 1996 (hereinafter referred to as “Non-patent Document 1”). Non-patent Document 1 discusses two elements: a control apparatus and a control target. In a control system including the two elements having a predetermined relationship therebetween, a control apparatus model M2 is generated from a model M of the specification of the control system (control specification) and a control target model M1. In Non-patent Document 1, these models are regarded as models of sequential machines.
In addition, in the fields of the above-described property checking, the properties (control specification) tend to be expressed as temporal logic expressions. The principal of the property checking is model checking. In model checking, a model of an object to be verified (tested) is expressed as the Kripke structure, and it is determined whether this Kripke structure model is a formula of a temporal logic, that is, it is determined whether this Kripke structure satisfies the temporal logic expressions.
Many documents have described model checking. For example, Japanese Patent No. 3600420 describes technology that efficiently performs model checking.
Additionally, it is common that a sequential machine is employed in a sequential circuit design. When the sequential machine is applied to model checking, a relationship between the sequential machine and a Kripke structure should be clearly defined. This relationship between the sequential machine and a Kripke structure is described by Hiromi HIRAISHI and Kiyoharu HAMAGUCHI, “Formal Verification Methods Based on Logic Function Manipulation” Journal of Information Processing Society of Japan, vol. 35 No. 8, August, 1994 (hereinafter referred to as “Non-patent Document 2”).
Also, E. M. Clarke, Orna Grumberg, and Doron Peled, “Model Checking”, MIT Press, ISBN: 0-262-03270-8, 2000 (hereinafter referred to as “Non-patent Document 3”) describes a method for creating a tableau from a temporal logic called linear temporal logic (LTL) or from a temporal logic called ACTL. In the ACTL, a temporal logic called computer tree logic (CTL) is restricted not to use an operator of E (possible), but to use only an operator of A (necessary).
As described above, the technology described in Non-patent Document 1 describes the creation of a control apparatus model M2 from a model M of the specification of the control system (control specification) and a control target model M1. This technology suggests that automatic design of the control apparatus model M2 is possible.
However, Non-patent Document 1 describes neither the detailed procedure of the automatic design of the control apparatus model M2 nor the detailed functional structure of an apparatus for providing the automatic design.
Furthermore, in Non-patent Document 1, the control specification model M is regarded as a sequential machine model. However, in general, as described in the model checking, a model M of the specification of a control system (control specification) defined as a temporal logic model is more accurate and simpler than that defined as a sequential machine model.